p(s(x)) → x
p(0) → 0
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y)
if(false, b1, b2, b3, x, y) → average(p(x), s(y))
if2(true, b2, b3, x, y) → 0
if2(false, b2, b3, x, y) → if3(b2, b3, x, y)
if3(true, b3, x, y) → 0
if3(false, b3, x, y) → if4(b3, x, y)
if4(true, x, y) → s(0)
if4(false, x, y) → average(s(x), p(p(y)))
↳ QTRS
↳ DependencyPairsProof
p(s(x)) → x
p(0) → 0
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y)
if(false, b1, b2, b3, x, y) → average(p(x), s(y))
if2(true, b2, b3, x, y) → 0
if2(false, b2, b3, x, y) → if3(b2, b3, x, y)
if3(true, b3, x, y) → 0
if3(false, b3, x, y) → if4(b3, x, y)
if4(true, x, y) → s(0)
if4(false, x, y) → average(s(x), p(p(y)))
AVERAGE(x, y) → LE(y, s(0))
IF(false, b1, b2, b3, x, y) → P(x)
IF(true, b1, b2, b3, x, y) → IF2(b1, b2, b3, x, y)
IF2(false, b2, b3, x, y) → IF3(b2, b3, x, y)
AVERAGE(x, y) → IF(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
IF(false, b1, b2, b3, x, y) → AVERAGE(p(x), s(y))
LE(s(x), s(y)) → LE(x, y)
IF4(false, x, y) → P(y)
IF4(false, x, y) → P(p(y))
IF4(false, x, y) → AVERAGE(s(x), p(p(y)))
IF3(false, b3, x, y) → IF4(b3, x, y)
AVERAGE(x, y) → LE(x, 0)
AVERAGE(x, y) → LE(y, 0)
AVERAGE(x, y) → LE(y, s(s(0)))
p(s(x)) → x
p(0) → 0
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y)
if(false, b1, b2, b3, x, y) → average(p(x), s(y))
if2(true, b2, b3, x, y) → 0
if2(false, b2, b3, x, y) → if3(b2, b3, x, y)
if3(true, b3, x, y) → 0
if3(false, b3, x, y) → if4(b3, x, y)
if4(true, x, y) → s(0)
if4(false, x, y) → average(s(x), p(p(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
AVERAGE(x, y) → LE(y, s(0))
IF(false, b1, b2, b3, x, y) → P(x)
IF(true, b1, b2, b3, x, y) → IF2(b1, b2, b3, x, y)
IF2(false, b2, b3, x, y) → IF3(b2, b3, x, y)
AVERAGE(x, y) → IF(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
IF(false, b1, b2, b3, x, y) → AVERAGE(p(x), s(y))
LE(s(x), s(y)) → LE(x, y)
IF4(false, x, y) → P(y)
IF4(false, x, y) → P(p(y))
IF4(false, x, y) → AVERAGE(s(x), p(p(y)))
IF3(false, b3, x, y) → IF4(b3, x, y)
AVERAGE(x, y) → LE(x, 0)
AVERAGE(x, y) → LE(y, 0)
AVERAGE(x, y) → LE(y, s(s(0)))
p(s(x)) → x
p(0) → 0
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y)
if(false, b1, b2, b3, x, y) → average(p(x), s(y))
if2(true, b2, b3, x, y) → 0
if2(false, b2, b3, x, y) → if3(b2, b3, x, y)
if3(true, b3, x, y) → 0
if3(false, b3, x, y) → if4(b3, x, y)
if4(true, x, y) → s(0)
if4(false, x, y) → average(s(x), p(p(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
LE(s(x), s(y)) → LE(x, y)
p(s(x)) → x
p(0) → 0
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y)
if(false, b1, b2, b3, x, y) → average(p(x), s(y))
if2(true, b2, b3, x, y) → 0
if2(false, b2, b3, x, y) → if3(b2, b3, x, y)
if3(true, b3, x, y) → 0
if3(false, b3, x, y) → if4(b3, x, y)
if4(true, x, y) → s(0)
if4(false, x, y) → average(s(x), p(p(y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LE(s(x), s(y)) → LE(x, y)
The value of delta used in the strict ordering is 1/4.
POL(s(x1)) = 1/2 + (4)x_1
POL(LE(x1, x2)) = (1/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
p(s(x)) → x
p(0) → 0
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y)
if(false, b1, b2, b3, x, y) → average(p(x), s(y))
if2(true, b2, b3, x, y) → 0
if2(false, b2, b3, x, y) → if3(b2, b3, x, y)
if3(true, b3, x, y) → 0
if3(false, b3, x, y) → if4(b3, x, y)
if4(true, x, y) → s(0)
if4(false, x, y) → average(s(x), p(p(y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
IF(true, b1, b2, b3, x, y) → IF2(b1, b2, b3, x, y)
IF4(false, x, y) → AVERAGE(s(x), p(p(y)))
IF2(false, b2, b3, x, y) → IF3(b2, b3, x, y)
IF3(false, b3, x, y) → IF4(b3, x, y)
AVERAGE(x, y) → IF(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
IF(false, b1, b2, b3, x, y) → AVERAGE(p(x), s(y))
p(s(x)) → x
p(0) → 0
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y)
if(false, b1, b2, b3, x, y) → average(p(x), s(y))
if2(true, b2, b3, x, y) → 0
if2(false, b2, b3, x, y) → if3(b2, b3, x, y)
if3(true, b3, x, y) → 0
if3(false, b3, x, y) → if4(b3, x, y)
if4(true, x, y) → s(0)
if4(false, x, y) → average(s(x), p(p(y)))